#lang planet plai/plai

;; Datatypes

(define-type Expr 
  [num (n number?)] 
  [id (v symbol?)] 
  [bool (b boolean?)] 
  [bin-num-op (op procedure?) (lhs Expr?) (rhs Expr?)] 
  [iszero (e Expr?)] 
  [bif (test Expr?) (then Expr?) (else Expr?)] 
  [with (bound-id symbol?) (bound-body Expr?) (body Expr?)] 
  [rec-with (bound-id symbol?) (bound-body Expr?) (body Expr?)] 
  [fun (arg-id symbol?) (body Expr?)] 
  [app (fun-expr Expr?) (arg-expr Expr?)] 
  [tempty] 
  [tcons (first Expr?) (rest Expr?)] 
  [tfirst (e Expr?)] 
  [trest (e Expr?)]
  [istempty (e Expr?)]) 

(define-type Type 
  [t-num] 
  [t-bool] 
  [t-list (elem Type?)] 
  [t-fun (arg Type?) (result Type?)] 
  [t-var (v symbol?)]) 

(define-type Constraint 
  [eqc (lhs Type?) (rhs Type?)])

(define-type Env
  [mtEnv]
  [anEnv (name symbol?) (unique-name symbol?) (next Env?)])

;;Suplemental code from the web-site for testing type and constraint list equality

; type=?/mapping : hash hash Type Type -> Bool 
; determines if types are equal modulo renaming 
(define (type=?/mapping ht1 ht2 t1 t2) 
  (define (teq? t1 t2) 
    (type=?/mapping ht1 ht2 t1 t2)) 
  (cond 
    [(and (t-num? t1) (t-num? t2)) true] 
    [(and (t-bool? t1) (t-bool? t2)) true] 
    [(and (t-list? t1) (t-list? t2)) 
     (teq? (t-list-elem t1) (t-list-elem t2))] 
    [(and (t-fun? t1) (t-fun? t2)) 
     (and (teq? (t-fun-arg t1) (t-fun-arg t2)) 
          (teq? (t-fun-result t1) (t-fun-result t2)))] 
    [(and (t-var? t1) (t-var? t2)) 
     (local ([define v1 ; the symbol that ht1 says that t1 maps to 
               (hash-ref 
                ht1 (t-var-v t1) 
                (lambda () 
                  ; if t1 doesn't map to anything, it's the first 
                  ; time we're seeing it, so map it to t2 
                  (hash-set! ht1 (t-var-v t1) (t-var-v t2)) 
                  (t-var-v t2)))] 
             [define v2 
               (hash-ref 
                ht2 (t-var-v t2) 
                (lambda () 
                  (hash-set! ht2 (t-var-v t2) (t-var-v t1)) 
                  (t-var-v t1)))]) 
       ; we have to check both mappings, so that distinct variables 
       ; are kept distinct. i.e. a -> b should not be isomorphic to 
       ; c -> c under the one-way mapping a => c, b => c. 
       (and (symbol=? (t-var-v t2) v1) 
            (symbol=? (t-var-v t1) v2)))] 
    [(and (Type? t1) (Type? t2)) false] 
    [else (error 'type=? "either ~a or ~a is not a Type" t1 t2)])) 

; type=? Type -> Type -> Bool 
; signals an error if arguments are not variants of Type 
(define ((type=? t1) t2) 
  (or (type=?/mapping (make-hash) (make-hash) t1 t2) 
      ; Unfortunately, test/pred simply prints false;  
      ; this helps us see what t2 was. 
      (error 'type=? 
             "~s and ~a are not equal (modulo renaming)" 
             t1 t2))) 

(test/pred (t-var 'a) 
           (type=? (t-var 'b))) 
(test/pred (t-fun (t-var 'a) (t-var 'b)) 
           (type=? (t-fun (t-var (gensym)) (t-var (gensym))))) 
(test/pred (t-fun (t-var 'a) (t-var 'b)) 
           (type=? (t-fun (t-var (gensym)) (t-var (gensym))))) 
(test/pred (t-fun (t-var 'a) (t-var 'a)) ; fails 
           (type=? (t-fun (t-var (gensym)) (t-var (gensym))))) 
(test/pred (t-fun (t-var 'a) (t-var 'b)) ; fails 
           (type=? (t-fun (t-var 'c) (t-var 'c)))) 
(test/exn ((type=? 34) 34) "not a Type") 

; constraint-list=? : Constraint list -> Constraint list -> Bool 
; signals an error if arguments are not variants of Constraint 
(define ((constraint-list=? lc1) lc2) 
  (define htlc1 (make-hash)) 
  (define htlc2 (make-hash)) 
  (or (andmap (lambda (c1 c2)  
                (and 
                 (type=?/mapping 
                  htlc1 htlc2 
                  (eqc-lhs c1) (eqc-lhs c2)) 
                 (type=?/mapping 
                  htlc1 htlc2 
                  (eqc-rhs c1) (eqc-rhs c2)))) 
              lc1 lc2) 
      (error 'constraint-list=? 
             "~s and ~a are not equal (modulo renaming)" 
             lc1 lc2))) 


;; ================================ OUR CODE STARTS HERE =======================================


;; Operator Table

;; Contract: op-table : (listof (list/c symbol? (number? number? . -> . number?)))

;; Purpose: mapping from operator symbols to their definitions

;; Example: (define op-table (list (list '+ +))) maps '+ symbol to the "+" arithmetical operation

;; Definition [refines the header]
(define op-table
  (list (list '+ +)(list '- -)(list '* *)))

;; Tests:
(display "===== Op-table tests =====\n")
(test (first (first op-table)) '+)
(test (second (first op-table)) +)


;; Contract: lookup-op symbol -> (or procedure boolean)

;; Purpose: to extract the arithmetical operation from the operator table based on the operator's symbol, or return false if the operator is not defined in the table.

;; Example: (lookup-op '+) should return "+" arithmetical operation,  (lookup-op '!) should return false, because the operator "!" is not defined in the table

;; Definition [refines the header]
(define (lookup-op op)
  (if (list? (assoc op op-table))
      (second (assoc op op-table))
      false))

;; Tests:
(display "\n====== Lookup-op tests ======\n")
(test (lookup-op '+) +)
(test (lookup-op '-) -)
(test (lookup-op '*) *)
(test (lookup-op '/) false)
(test (lookup-op '!) false)
(test (lookup-op '$) false)



;; Contract:  parse : s-expression -> Expr 

;; Purpose: consumes the concrete representation of a program, and returns its abstract syntax tree

;; Example: (parse '{+ 1 2}) should return (bin-num-op + (num 1) (num 2))

;; Definition [refines the header]
(define (parse sexp)
  (cond
    [(number? sexp) (num sexp)]                      ; parsing number
    [(boolean? sexp) (bool sexp)]                    ; parsing boolean
    [(symbol? sexp)                                  ; parsing id
     (if(or
         (symbol=? sexp '+)
         (symbol=? sexp '-)
         (symbol=? sexp '*)
         (symbol=? sexp 'iszero)
         (symbol=? sexp 'bif)
         (symbol=? sexp 'with)
         (symbol=? sexp 'rec)
         (symbol=? sexp 'fun)
         (symbol=? sexp 'tcons)
         )
        (error 'parse "Invalid id")
        (cond
          [(symbol=? sexp 'true) (bool true)]
          [(symbol=? sexp 'false) (bool false)]
          [(symbol=? sexp 'tempty) (tempty)]
          #|[(symbol=? sexp 'number) (t-num)]
          [(symbol=? sexp 'boolean) (t-bool)]
          [(symbol=? sexp 'list) (t-list)] |#
          [true (id sexp)]))
     ]
    [(list? sexp)                                    ; parsing binding and +/- operations
     (if (= (length sexp) 1)
         (error 'parse "Invalid syntax: no operator is allowed without arguments")
         (if (= (length sexp) 2)                         ; processing operators that take 1 argument
             (cond
               [(equal? (first sexp) 'with) (error 'parse "with can't take less than 2 argument")]
               [(equal? (first sexp) 'rec-with) (error 'parse "rec-with can't take less than 2 argument")]
               [(equal? (first sexp) 'tcons) (error 'parse "tcons can't take less than 2 arguments")]
               [(equal? (first sexp) 'bif) (error 'parse "bif takes exactly 3 arguments")]
               [(equal? (first sexp) 'iszero) (iszero (parse(second sexp)))]
               [(equal? (first sexp) 'fun) (error 'parse "fun: Invalid syntax")]
               [(equal? (first sexp) 'tfirst) (tfirst (parse(second sexp)))]
               [(equal? (first sexp) 'trest) (trest (parse(second sexp)))]
               [(equal? (first sexp) 'tempty?) (istempty (parse(second sexp)))]
               [true (app (first (map parse sexp)) (second (map parse sexp))) ])            ; List of Expr (app expr expr)
             (if (= (length sexp) 3)                     ; processing operators that take only 2 arguments
                 
                 (cond [(not(equal? (lookup-op (first sexp)) false))    ; check if we got a valid operator
                        (bin-num-op (lookup-op (first sexp)) (parse (second sexp))
                                    (parse (third sexp)))]
                       
                       [(equal? (first sexp) 'tcons) (tcons (parse(second sexp)) (parse (third sexp)))]
                       [(equal? (first sexp) 'iszero) (error 'parse "iszero can't take more than 1 argument")]
                       [(equal? (first sexp) 'bif) (error 'parse "bif takes exactly 3 arguments")]
                       [(equal? (first sexp) 'fun) 
                        (if (and
                             (symbol? (first(second sexp)))
                             (= (length (second sexp)) 1))
                            (fun (first(second sexp)) (parse (third sexp)))
                            (error 'parse "fun takes a single symbol as its argument"))]
                       
                       [(equal? (first sexp) 'with)
                        (if (symbol? (first (second sexp)))             
                            
                            (with 
                             (first (second sexp))           ; first element of the first binding
                             (parse (second (second sexp))) ; with parsed seconds element of the first binding
                             (parse (third sexp)))
                            
                            (error 'parse "Not a binding passed to 'with'"))]
                       
                       
                       [(equal? (first sexp) 'rec)
                        (if (symbol? (first (second sexp)))                    
                            
                            (rec-with 
                             (first (second sexp))           ; first element of the first binding
                             (parse (second (second sexp))) ; with parsed seconds element of the first binding
                             (parse (third sexp)))
                            
                            (error 'parse "Not a binding passed to 'with'"))]
                       
                       [(equal? (first sexp) 'fun) (error 'parse "fun takes exactly 4 arguments")]
                       [(Type? (parse (first sexp))) (t-fun (parse(first sexp)) (parse (third sexp)))]
                       [true (error 'parse "Invalid operator name")]                    
                       )
                 (if (= (length sexp) 4)                     ; processing operators that take only 3 arguments
                     (cond  
                       [(equal? (first sexp) 'iszero) (error 'parse "iszero can't take more than 1 argument")]
                       [(equal? (first sexp) 'with) (error 'parse "with can't take more than 2 arguments")]
                       [(equal? (first sexp) 'rec-with) (error 'parse "rec-with can't take more than 2 arguments")]
                       [(not(equal? (lookup-op (first sexp)) false)) (error 'parse "Operator can't take more than two arguments")]
                       [(equal? (first sexp) 'bif) (bif (parse (second sexp)) (parse(third sexp)) (parse (fourth sexp)))]
                       [(equal? (first sexp) 'fun) (error 'parse "fun: Invalid syntax")]
                       [(equal? (first sexp) 'tcons) (error 'parse "tcons can't take more than 2 arguments")]
                       [true (error 'parse "Invalid operator name")])
                     (error 'parse "Operator or construct can't take more than three arguments")                     
                     ))))]
    [true (error 'parse "Illegal syntax")]))                           ; illegal datatype argument

;; Tests:
(display "\n====== Parser tests ======\n")
(test/exn (parse "foobar") "Illegal syntax")                                            ;; Test invalid expression - don't parse strings
'num:
(test (parse '5) (num 5))                                                               ;; Test num

'id:
(test (parse 'a) (id 'a))                                                               ;; Test id
(test (parse '!) (id '!))                                                               ;; Weird id test
(test/exn (parse '+) "Invalid id")                                                      ;; Invalid id test
(test/exn (parse 'with) "Invalid id")                                                   ;; Invalid id test
;; the following test cases are to make sure that I removed the types from the language concrete syntax
(test (parse 'number) (id 'number))
(test (parse 'boolean) (id 'boolean))
(test (parse 'list) (id 'list))

'boolean:
(test (parse 'true) (bool #t))                                                           ;; test boolean
(test (parse 'false) (bool #f))                                                          ;; test boolean
(test (parse '#t) (bool #t))                                                             ;; test boolean
(test (parse '#f) (bool #f))                                                             ;; test boolean

'bin-num-op:
(test (parse '(+ 1 2)) (bin-num-op + (num 1) (num 2)))                                  ;; Test bin-num-op - legal
(test/exn (parse '(! 1 2)) "Invalid operator name")                                     ;; Test bin-num-op - illegal op
(test/exn (parse '(+ 1 2 3)) "Operator can't take more than two arguments")             ;; Test bin-num-op - more args

'iszero:
(test (parse '{iszero 0}) (iszero (num 0)))                                             ;; Test iszero on num
(test (parse '{iszero abc}) (iszero (id 'abc)))                                         ;; Test iszero on id
(test/exn (parse '{iszero 0 1}) "iszero can't take more than 1 argument")               ;; Test is zero with more than 1 argument

'bif:
(test (parse '{bif true false true}) (bif (bool #t) (bool #f) (bool #t)))               ;; Testing bif correct args
(test (parse '(bif 0 1 2)) (bif (num 0) (num 1) (num 2)))                               ;; Error during evaluation, but parse should be fine
(test (parse '{bif #t #f #t}) (bif (bool #t) (bool #f) (bool #t)))                      ;; Testing bif correct args
(test (parse '{bif #t #f #t}) (bif (bool #t) (bool #f) (bool #t)))                      ;; Testing bif correct args
(test/exn (parse '{bif #t}) "bif takes exactly 3 arguments")                            ;; Testing bif invalid number of args
(test/exn (parse '{bif false #f}) "bif takes exactly 3 arguments")                      ;; Testing bif invalid number of args
(test/exn (parse '{bif true #t #f false}) "parse: Operator or construct can't take more than three arguments");; Testing bif invalid number of args

'with:
(test (parse '(with [x 1] y)) (with 'x (num 1) (id 'y)))                                ;; with simple test
(test (parse '(with [x 1] (* x 2))) (with 'x (num 1) (bin-num-op * (id 'x) (num 2))))   ;; with expression test
(test (parse '(with (x 5) (+ x x)))  (with 'x (num 5) (bin-num-op + (id 'x) (id 'x))))  ;; one more
(test/exn (parse '(with [3 3] x)) "Not a binding passed to 'with'")                     ;; Malformed binding
(test (parse '(with (x x) 10)) (with 'x (id 'x) (num 10)))                              ;; Scopping test
(test (parse '(with [x 1] (with [y 2] (with [z 3] {- x {+ y z}}))))                     ;; Enclosed 'with' test
      (with 'x (num 1)
            (with 'y (num 2)
                  (with 'z (num 3)
                        (bin-num-op - (id 'x) (bin-num-op + (id 'y) (id 'z)))))))

'rec-with:
(test (parse '(rec [x 1] y)) (rec-with 'x (num 1) (id 'y)))                            ;; rec simple test
(test (parse '(rec [x 1] (* x 2))) (rec-with 'x (num 1) (bin-num-op * (id 'x) (num 2))));; with expression test
(test (parse '(rec (x 5) (+ x x)))  (rec-with 'x (num 5) (bin-num-op + (id 'x) (id 'x))))  ;; one more
(test/exn (parse '(rec [3 3] x)) "Not a binding passed to 'with'")                     ;; Malformed binding
(test (parse '(rec (x x) 10)) (rec-with 'x (id 'x) (num 10)))                          ;; Scopping test
(test (parse '(rec [x 1] (rec [y 2] (rec [z 3] {- x {+ y z}}))))                       ;; Enclosed 'with' test
      (rec-with 'x (num 1)
                (rec-with 'y (num 2)
                          (rec-with 'z (num 3)
                                    (bin-num-op - (id 'x) (bin-num-op + (id 'y) (id 'z)))))))

'fun:
(test (parse '(fun (x) 10)) (fun 'x (num 10)))                                           ;; fun: Simple case
(test/exn (parse '(fun (x wrong) 10)) "fun takes a single symbol as its argument")       ;; fun: ok, we din't bullet-prove it
(test/exn (parse '(fun (x : number) number 10)) "fun: Invalid syntax")                   ;; fun: Invalid syntax - too many args
(test/exn (parse '(fun (1) test)) "fun takes a single symbol as its argument")           ;; fun: Invalid syntax
(test/exn (parse '(fun (x : ) : number 10)) "parse: Operator or construct can't take more than three arguments");; fun: Invalid syntax
(test (parse '(fun (x) (+ x x))) (fun 'x (bin-num-op + (id 'x) (id 'x))))                ;; fun: Complex case 

'app:
(test (parse '{x 1}) (app (id 'x) (num 1)))                                             ;; simple app test
(test (parse '{true #f}) (app (bool true) (bool false)))                                ;; simple app test (different datatypes)
(test (parse '{{+ 1 x} false}) (app (bin-num-op + (num 1) (id 'x)) (bool #f)))          ;; complex app test
(test/exn (parse '{x 1 #t}) "Invalid operator name")                                    ;; invalid syntax test
(test/exn (parse '{x 1 #t false})  "Invalid operator name")                             ;; invalid syntax test
(test/exn (parse '{x}) "Invalid syntax: no operator is allowed without arguments")      ;; invalid syntax test
(test (parse '{boolean number}) (app (id 'boolean)  (id 'number)))
(test (parse '{{list boolean} number}) (app (app (id 'list)(id 'boolean))(id 'number)))
(test (parse '{{fun (x) 10} input}) (app (fun 'x (num 10)) (id 'input)))
'tempty:
(test (parse 'tempty) (tempty))

'tcons:
(test (parse '{tcons 1 2}) (tcons (num 1) (num 2)))                                     ;; generic cons test
(test (parse '{tcons x false}) (tcons (id 'x) (bool false)))                            ;; another generic cons
(test (parse '{tcons 1 tempty}) (tcons (num 1) (tempty)))                               ;; a real cons
(test (parse '{tcons 1 {tcons 2 tempty}}) (tcons (num 1) (tcons (num 2) (tempty))))     ;; a list
(test/exn (parse '{tcons 1}) "tcons can't take less than 2 arguments")                  ;; malformed cons
(test/exn (parse '{tcons}) "Invalid syntax: no operator is allowed without arguments")  ;; malformed cons
(test/exn (parse '{tcons 1 x #t}) "tcons can't take more than 2 arguments")             ;; malformed cons
(test/exn (parse '{tcons 1 x #t number}) "Operator or construct can't take more than three arguments")   ;; malformed cons
(test/exn (parse '{tcons 1 x #t false number}) "Operator or construct can't take more than three arguments")   ;; malformed cons
(test (parse '(tcons (fun (x) true) (iszero x))) (tcons (fun 'x (bool true)) (iszero (id 'x)))) ; passing is okay, but typeinferrer should complain

'tfirst:
(test (parse '{tfirst 1}) (tfirst (num 1)))                                                                   ;; generic tfirst
(test/exn (parse '{tfirst 1 2}) "Invalid operator name")                                                      ;; invalid syntax
(test/exn (parse '{tfirst}) "Invalid syntax: no operator is allowed without arguments")                       ;; invalid syntax
(test (parse '{tfirst {tcons 1 {tcons 2 tempty}}}) (tfirst (tcons (num 1) (tcons (num 2) (tempty)))))         ;; real tfirst usage

'trest:
(test (parse '{trest 1}) (trest (num 1)))                                                                     ;; generic trest
(test/exn (parse '{trest 1 2}) "Invalid operator name")                                                       ;; invalid syntax
(test/exn (parse '{trest}) "Invalid syntax: no operator is allowed without arguments")                        ;; invalid syntax
(test (parse '{trest {tcons 1 {tcons 2 tempty}}}) (trest (tcons (num 1) (tcons (num 2) (tempty)))))           ;; real trest usage

'tempty?:
(test (parse '{tempty? 1}) (istempty (num 1)))                                                                ;; generic istempty
(test/exn (parse '{tempty? 1 2}) "Invalid operator name")                                                     ;; invalid syntax
(test/exn (parse '{tempty?}) "Invalid syntax: no operator is allowed without arguments")                      ;; invalid syntax
(test (parse '{tempty? {tcons 1 {tcons 2 tempty}}}) (istempty (tcons (num 1) (tcons (num 2) (tempty)))))      ;; real istempty usage

'combined:
(test (parse '((fun (x) (+ x x)) (tcons 2 tempty)))
      (app (fun 'x (bin-num-op + (id 'x) (id 'x))) (tcons (num 2) (tempty))))
(test (parse '(with (x (tcons 1 (tcons false tempty))) x)) (with 'x (tcons (num 1) (tcons (bool #f) (tempty))) (id 'x)))
(test (parse '(with [x true] (with [y (tcons 2 (tcons a tempty))] (with [z 3] {- x {+ y z}}))))
      (with 'x (bool true)
            (with 'y (tcons (num 2) (tcons (id 'a) (tempty)))
                  (with 'z (num 3)
                        (bin-num-op - (id 'x) (bin-num-op + (id 'y) (id 'z)))))))



;===========================================  alpha-vary  ================================================= 
;Contract: lookup symbol Env -> symbol
;Purpose: looks up symbol var-name in the environment, and returns that variable's name is present, else gives it a new name
;;Examples: (see test)
;; Definition [refines the header]:
(define (lookup var-name env)
  (type-case Env env 
             [mtEnv () (gensym var-name)]
             [anEnv (name unique-name next) (if (symbol=? name var-name) unique-name (lookup var-name next))]))

;Contract: alpha-vary Expr -> Expr
;Purpose: calls alpha-varyE with an empty environment. give all variables a unique id. 
;;Examples: (see test)
;; Definition [refines the header]:
(define (alpha-vary e)
  (alpha-varyE e (mtEnv)))

;Contract: alpha-varyE Expr Env -> Expr
;Purpose: give all variables a unique id, and uses the environment to remember which variables are identical
;;Examples: (see test)
;; Definition [refines the header]:
(define (alpha-varyE e env) 
  (type-case Expr e
             [num (n) (num n)]
             [id (v) (id (lookup v env))]
             [bool (b) (bool b)]
             [bin-num-op (op lhs rhs) (bin-num-op op (alpha-varyE lhs env) (alpha-varyE rhs env))]
             [iszero (e1) (iszero (alpha-varyE e1 env))]
             [bif (test then else) (bif (alpha-varyE test env) (alpha-varyE then env) (alpha-varyE else env))]
             [with (bound-id bound-body body) 
                   (local 
                     [(define uniqued-bound-id (gensym bound-id))] 
                     (with uniqued-bound-id (alpha-varyE bound-body env) (alpha-varyE body (anEnv bound-id uniqued-bound-id env))))]
             [rec-with (bound-id bound-body body) 
                       (local 
                         [(define uniqued-bound-id (gensym bound-id))] 
                         (rec-with uniqued-bound-id (alpha-varyE bound-body env) (alpha-varyE body (anEnv bound-id uniqued-bound-id env))))]
             [fun (arg-id body) (local 
                                  [(define unique-arg-id (gensym arg-id))]
                                  (fun unique-arg-id (alpha-varyE body (anEnv arg-id unique-arg-id env))))]
             [app (fun-expr arg-expr) (app (alpha-varyE fun-expr env) (alpha-varyE arg-expr env))]
             [tempty () (tempty)]
             [tcons (first rest) (tcons (alpha-varyE first env) (alpha-varyE rest env))]
             [tfirst (e1) (tfirst (alpha-varyE e1 env))]
             [trest (e1) (trest (alpha-varyE e1 env))]
             [istempty (e1) (istempty (alpha-varyE e1 env))]))

;; Test [most of the passing tests need to be verified manually because "alpha-vary" prevents from automating them]:
"alpha-vary tests"
;test num
(test (alpha-varyE (num 1) (mtEnv)) (num 1))
(alpha-varyE (id 'x) (mtEnv))
(test (alpha-varyE (bool true) (mtEnv)) (bool true)) 
(test (alpha-varyE (bin-num-op + (num 1) (bool false)) (mtEnv)) (bin-num-op + (num 1) (bool false)))
(alpha-varyE (with 'x (num 2) (id 'x))(mtEnv))
(alpha-varyE (with 'x (num 2) (bin-num-op + (num 1) (id 'x)))(mtEnv))
(alpha-varyE (with 'x (num 2) (with 'x (num 3) (id 'x)))(mtEnv))
(alpha-varyE (fun 'x (id 'x)) (mtEnv))
(alpha-varyE (fun 'x (bin-num-op + (num 2) (id 'x)))(mtEnv))
(alpha-varyE (app (fun 'x (bin-num-op + (num 2) (id 'x))) (num 5)) (mtEnv))
(alpha-varyE (rec-with 'x (num 3) (id 'x))(mtEnv))
(alpha-varyE (tempty) (mtEnv))
(alpha-vary (tcons (id 'x) (tempty)))
(alpha-vary (tcons (id 'x) (tcons (with 'x (num 1) (id 'x)) (tempty))))
(alpha-vary (tfirst (tcons (with 'x (num 1) (id 'x)) (tempty))))
(alpha-vary (trest (tcons (num 1) (tcons (with 'x (num 2) (id 'x)) (tempty)))))
(alpha-vary (istempty (tcons (with 'x (num 2) (id 'x)) (tempty))))
;----------------------------------------- constraint-generator ---------------------------------------------
;Contract: symbol, Expr -> listOfConstraints
;Purpose: call generate-constraintsC with an empty list of constraints. to get the constraints for Expr
;;Examples: (see test)
;; Definition [refines the header]:
(define (generate-constraints e-id e)
  (generate-constraintsC e-id e empty))

;Contract: symbol, Expr, listOfConstraints -> listOfConstraints
;Purpose: return the constraints for this expression PLUS the constraints passed in
;;Examples: (see test)
;; Definition [refines the header]:
(define (generate-constraintsC e-id e constraints)
  (type-case Expr e
             [num (n) (cons (eqc (t-var e-id) (t-num)) constraints)]
             [id (v) (cons (eqc (t-var e-id) (t-var v)) constraints)]
             [bool (b) (cons (eqc (t-var e-id) (t-bool)) constraints)]
             [bin-num-op (op lhs rhs) (local
                                        [(define lhsID (gensym 'addlhs))
                                         (define rhsID (gensym 'addrhs))]
                                        (cons (eqc (t-var e-id) (t-num)) 
                                              (cons (eqc (t-var lhsID) (t-num))
                                                    (cons (eqc (t-var rhsID) (t-num)) 
                                                          (generate-constraintsC lhsID lhs (generate-constraintsC rhsID rhs constraints))))))]
             [iszero (expr) (local
                              [(define exprID (gensym 'zeroBody))]
                              (cons (eqc (t-var e-id) (t-bool)) ;[wholeExpression]=bool
                                    (cons (eqc (t-var exprID) (t-num)) ;[test]=num
                                          (generate-constraintsC exprID expr constraints))))]
             [bif (test then else) (local
                                     [(define testID (gensym 'test))
                                      (define thenID (gensym 'then))
                                      (define elseID (gensym 'else))]
                                     (cons (eqc (t-var e-id) (t-var thenID)) ;[wholeExpression] =[then] or [else]
                                           (cons (eqc (t-var testID) (t-bool)) ;[test]=bool
                                                 (cons (eqc (t-var thenID) (t-var elseID)) ;[then]=[else]
                                                       (generate-constraintsC testID test 
                                                                              (generate-constraintsC thenID then 
                                                                                                     (generate-constraintsC elseID else constraints)))))))]
             [with (bound-id bound-body body) (local [(define bodyID (gensym 'withBody))
                                                      (define boundBodyID (gensym 'boundBody))]
                                                (cons (eqc (t-var e-id) (t-var bodyID)) ;with returns whatever body returns
                                                      (cons (eqc (t-var bound-id) (t-var boundBodyID)) ;[id]=[bound-body]
                                                            (generate-constraintsC boundBodyID bound-body ;find [bound-body]
                                                                                   (generate-constraintsC bodyID body constraints)))))] ;find [body]
             [rec-with (bound-id bound-body body ) (local [(define bodyID (gensym 'withBody))
                                                           (define boundBodyID (gensym 'boundBody))]
                                                     (cons (eqc (t-var e-id) (t-var bodyID)) ;with returns whatever body returns
                                                           (cons (eqc (t-var bound-id) (t-var boundBodyID)) ;[id]=[bound-body]
                                                                 (generate-constraintsC boundBodyID bound-body ;find [bound-body]
                                                                                        (generate-constraintsC bodyID body constraints)))))] ;find [body]
             [fun (arg-id body) (local
                                  [(define bodyID (gensym 'bodyID))]
                                  (cons (eqc (t-var e-id) (t-fun (t-var arg-id) (t-var bodyID))) ;[fun]=[id]->[body]
                                        (generate-constraintsC bodyID body constraints)))] ;find [body]
             [app (fun-expr arg-expr) (local
                                        [(define fun-exprID (gensym 'funExpr))
                                         (define arg-exprID (gensym 'argExpr))
                                         (define unknownReturnID (gensym 'funReturn))]
                                        (cons (eqc (t-var e-id) (t-var unknownReturnID)) ;[app]=[unknown, whatever fun-expr returns]
                                              (cons (eqc (t-var fun-exprID) (t-fun (t-var arg-exprID) (t-var unknownReturnID))) ;[fun]=[arg-expr]->[unknown, whatever fun-expr returns]
                                                    (generate-constraintsC arg-exprID arg-expr ;find [arg-expr]
                                                                           (generate-constraintsC fun-exprID fun-expr constraints)))))] ;find [fun-expr]
             [tempty () (cons (eqc (t-var e-id) (t-list (t-var (gensym 'emptyElements)))) constraints)]
             [tcons (first rest) (local
                                   [(define elementID (gensym 'element))
                                    (define restID (gensym 'rest))]
                                   (cons (eqc (t-var e-id) (t-list (t-var elementID))) ;[wholeExpression]=listof([element])
                                         (cons (eqc (t-var restID) (t-list (t-var elementID))) ;[rest]=listof([element])
                                               (generate-constraintsC elementID first
                                                                      (generate-constraintsC restID rest constraints)))))]
             [tfirst (expr) (local
                              [(define listTypeID (gensym 'tfirstListType))
                               (define tfirstInputID (gensym 'tfirstInput))]
                              (cons (eqc (t-var e-id) (t-var listTypeID))
                                    (cons (eqc (t-var tfirstInputID) (t-list (t-var listTypeID)))
                                          (generate-constraintsC tfirstInputID expr constraints))))]
             [trest (expr) (local 
                             [(define exprID (gensym 'inrest))
                              (define listElementID (gensym 'restElementID))]
                             (cons (eqc (t-var e-id) (t-var exprID))
                                   (cons (eqc (t-var exprID) (t-list (t-var listElementID)))
                                         (generate-constraintsC exprID expr constraints))))]
             [istempty (test) (local
                                [(define istemptyInputID (gensym 'istemptyInput))
                                 (define listElementID (gensym 'istemptyElementID))]
                                (cons (eqc (t-var e-id) (t-bool))
                                      (cons (eqc (t-var istemptyInputID) (t-list (t-var listElementID)))
                                            (generate-constraintsC istemptyInputID test constraints))))])) 


;; Test [most of the passing tests need to be verified manually because "alpha-vary" prevents from automating them]:

"generate-constraints tests"  ;; automate them
((constraint-list=? (generate-constraints 'x234 (num 1))) (list (eqc (t-var 'x) (t-num)))) 
((constraint-list=? (generate-constraints 'x54 (id 'x54))) (list (eqc (t-var 'x) (t-var 'x)))) 
((constraint-list=? (generate-constraints 'x123 (bool false))) (list (eqc (t-var 'x) (t-bool))))

((constraint-list=? (generate-constraints 'wholeThing (bin-num-op + (bool false) (bool false)))) 
 (list (eqc (t-var 'wholeThing) (t-num))
       (eqc (t-var 'addlhs) (t-num))
       (eqc (t-var 'addrhs) (t-num))
       (eqc (t-var 'addlhs) (t-bool))
       (eqc (t-var 'addrhs) (t-bool))))
((constraint-list=? (generate-constraints 'wholeThing (bin-num-op + (bool false) (num 2)))) 
 (list (eqc (t-var 'wholeThing) (t-num))
       (eqc (t-var 'addlhs) (t-num))
       (eqc (t-var 'addrhs) (t-num))
       (eqc (t-var 'addlhs) (t-bool))
       (eqc (t-var 'addrhs) (t-num))))
((constraint-list=? (generate-constraints 'wholeThingProb (bin-num-op + (bin-num-op + (num 1) (num 2)) (num 3))))
 (list (eqc (t-var 'wholeThingProb) (t-num))
       (eqc (t-var 'addlhs17476) (t-num))
       (eqc (t-var 'addrhs17477) (t-num))
       (eqc (t-var 'addlhs17476) (t-num))
       (eqc (t-var 'addlhs17478) (t-num))
       (eqc (t-var 'addrhs17479) (t-num))
       (eqc (t-var 'addlhs17478) (t-num))
       (eqc (t-var 'addrhs17479) (t-num))
       (eqc (t-var 'addrhs17477) (t-num))))
((constraint-list=? (generate-constraints 'zeroTest (iszero (bool false)))) 
 (list (eqc (t-var 'zeroTest) (t-bool)) (eqc (t-var 'zeroBody4176) (t-num)) (eqc (t-var 'zeroBody4176) (t-bool))))
((constraint-list=? (generate-constraints 'bifTest (bif (bool false) (num 2) (num 3))))
 (list (eqc (t-var 'bifTest) (t-var 'then16749)) (eqc (t-var 'test16748) (t-bool)) (eqc (t-var 'then16749) (t-var 'else16750)) (eqc (t-var 'test16748) (t-bool)) (eqc (t-var 'then16749) (t-num)) (eqc (t-var 'else16750) (t-num))))

((constraint-list=? (generate-constraints 'empptTest (tempty))) 
 (list (eqc (t-var 'empptTest) (t-list (t-var 'emptyElements)))))
((constraint-list=? (generate-constraints 'consTest (tcons (num 1) (tcons (bool false) (tempty))))) 
 (list (eqc (t-var 'consTest) (t-list (t-var 'element4181)))
       (eqc (t-var 'rest4182) (t-list (t-var 'element4181)))
       (eqc (t-var 'element4181) (t-num))
       (eqc (t-var 'rest4182) (t-list (t-var 'element4183)))
       (eqc (t-var 'rest4184) (t-list (t-var 'element4183)))
       (eqc (t-var 'element4183) (t-bool))
       (eqc (t-var 'rest4184) (t-list (t-var 'emptyElements4185))))) 
((constraint-list=? (generate-constraints 'firstTest (tfirst (tcons (num 1) (tempty)))))
 (list (eqc (t-var 'firstTest) (t-var 'tfirstListType5227))
       (eqc (t-var 'tfirstInput5228) (t-list (t-var 'tfirstListType5227)))
       (eqc (t-var 'tfirstInput5228) (t-list (t-var 'element5229)))
       (eqc (t-var 'rest5230) (t-list (t-var 'element5229)))
       (eqc (t-var 'element5229) (t-num))
       (eqc (t-var 'rest5230) (t-list (t-var 'emptyElements5231)))))

((constraint-list=? (generate-constraints 'restTest (trest (tcons (num 1) (tempty)))))
 (list (eqc (t-var 'restTest) (t-var 'inrest5232))
       (eqc (t-var 'inrest5232) (t-list (t-var 'restElementID5233)))
       (eqc (t-var 'inrest5232) (t-list (t-var 'element5234)))
       (eqc (t-var 'rest5235) (t-list (t-var 'element5234)))
       (eqc (t-var 'element5234) (t-num))
       (eqc (t-var 'rest5235) (t-list (t-var 'emptyElements5236)))))
((constraint-list=? (generate-constraints 'restTest (trest (num 1))))
 (list (eqc (t-var 'restTest) (t-var 'inrest5237)) (eqc (t-var 'inrest5237) (t-list (t-var 'restElementID5238))) (eqc (t-var 'inrest5237) (t-num))))
((constraint-list=? (generate-constraints 'isemptyTest (istempty (tcons (num 1) (tempty)))))
 (list (eqc (t-var 'isemptyTest) (t-bool))
       (eqc (t-var 'istemptyInput5239) (t-list (t-var 'istemptyElementID5240)))
       (eqc (t-var 'istemptyInput5239) (t-list (t-var 'element5241)))
       (eqc (t-var 'rest5242) (t-list (t-var 'element5241)))
       (eqc (t-var 'element5241) (t-num))
       (eqc (t-var 'rest5242) (t-list (t-var 'emptyElements5243)))))
((constraint-list=? (generate-constraints 'withTest (with 'x (num 1) (bin-num-op + (id 'x) (num 2)))))
 (list (eqc (t-var 'withTest) (t-var 'withBody5244))
       (eqc (t-var 'x) (t-var 'boundBody5245))
       (eqc (t-var 'boundBody5245) (t-num))
       (eqc (t-var 'withBody5244) (t-num))
       (eqc (t-var 'addlhs5246) (t-num))
       (eqc (t-var 'addrhs5247) (t-num))
       (eqc (t-var 'addlhs5246) (t-var 'x))
       (eqc (t-var 'addrhs5247) (t-num))))
((constraint-list=? (generate-constraints 'funTest (fun 'x (num 4))))
 (list (eqc (t-var 'funTest) (t-fun (t-var 'x) (t-var 'bodyID5248))) (eqc (t-var 'bodyID5248) (t-num))))
((constraint-list=? (generate-constraints 'funTest2 (fun 'x (bin-num-op + (num 1) (id 'x)))))
 (list (eqc (t-var 'funTest2) (t-fun (t-var 'x) (t-var 'bodyID5999)))
       (eqc (t-var 'bodyID5999) (t-num))
       (eqc (t-var 'addlhs6000) (t-num))
       (eqc (t-var 'addrhs6001) (t-num))
       (eqc (t-var 'addlhs6000) (t-num))
       (eqc (t-var 'addrhs6001) (t-var 'x))))
((constraint-list=? (generate-constraints 'appTest (app (fun 'x (bin-num-op + (num 1) (id 'x))) (bool false))))
 (list (eqc (t-var 'appTest) (t-var 'funReturn6004))
       (eqc (t-var 'funExpr6002) (t-fun (t-var 'argExpr6003) (t-var 'funReturn6004)))
       (eqc (t-var 'argExpr6003) (t-bool))
       (eqc (t-var 'funExpr6002) (t-fun (t-var 'x) (t-var 'bodyID6005)))
       (eqc (t-var 'bodyID6005) (t-num))
       (eqc (t-var 'addlhs6006) (t-num))
       (eqc (t-var 'addrhs6007) (t-num))
       (eqc (t-var 'addlhs6006) (t-num))
       (eqc (t-var 'addrhs6007) (t-var 'x))))
((constraint-list=? (generate-constraints 'apptest2 (with 'x (fun 'f (bool false)) (app (id 'x) (num 1)))))
 (list (eqc (t-var 'apptest2) (t-var 'withBody6008))
       (eqc (t-var 'x) (t-var 'boundBody6009))
       (eqc (t-var 'boundBody6009) (t-fun (t-var 'f) (t-var 'bodyID6013)))
       (eqc (t-var 'bodyID6013) (t-bool))
       (eqc (t-var 'withBody6008) (t-var 'funReturn6012))
       (eqc (t-var 'funExpr6010) (t-fun (t-var 'argExpr6011) (t-var 'funReturn6012)))
       (eqc (t-var 'argExpr6011) (t-num))
       (eqc (t-var 'funExpr6010) (t-var 'x))))
((constraint-list=? (generate-constraints 'withList (with 'x (tcons (num 1) (tempty)) (tfirst (id 'x)))))
 (list (eqc (t-var 'withList) (t-var 'withBody6014))
       (eqc (t-var 'x) (t-var 'boundBody6015))
       (eqc (t-var 'boundBody6015) (t-list (t-var 'element6018)))
       (eqc (t-var 'rest6019) (t-list (t-var 'element6018)))
       (eqc (t-var 'element6018) (t-num))
       (eqc (t-var 'rest6019) (t-list (t-var 'emptyElements6020)))
       (eqc (t-var 'withBody6014) (t-var 'tfirstListType6016))
       (eqc (t-var 'tfirstInput6017) (t-list (t-var 'tfirstListType6016)))
       (eqc (t-var 'tfirstInput6017) (t-var 'x))))

"tests everything up to generate-constraints"
((constraint-list=? (generate-constraints 'wholeThing1 (alpha-vary (parse 'true))))
 (list (eqc (t-var 'wholeThing1) (t-bool))))
((constraint-list=? (generate-constraints 'wholeThing2 (alpha-vary (parse '12))))
 (list (eqc (t-var 'wholeThing2) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing3 (alpha-vary (parse '(+ 34 false)))))
 (list (eqc (t-var 'wholeThing3) (t-num))
       (eqc (t-var 'addlhs6790) (t-num))
       (eqc (t-var 'addrhs6791) (t-num))
       (eqc (t-var 'addlhs6790) (t-num))
       (eqc (t-var 'addrhs6791) (t-bool))))
((constraint-list=? (generate-constraints 'wholeThing4 (alpha-vary (parse '(with (x 34) (+ x 1))))))
 (list (eqc (t-var 'wholeThing4) (t-var 'withBody6793))
       (eqc (t-var 'x6792) (t-var 'boundBody6794))
       (eqc (t-var 'boundBody6794) (t-num))
       (eqc (t-var 'withBody6793) (t-num))
       (eqc (t-var 'addlhs6795) (t-num))
       (eqc (t-var 'addrhs6796) (t-num))
       (eqc (t-var 'addlhs6795) (t-var 'x6792))
       (eqc (t-var 'addrhs6796) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing5 (alpha-vary (parse '(iszero false)))))
 (list (eqc (t-var 'wholeThing5) (t-bool)) (eqc (t-var 'zeroBody6797) (t-num)) (eqc (t-var 'zeroBody6797) (t-bool))))
((constraint-list=? (generate-constraints 'wholeThing6 (alpha-vary (parse '(iszero 34)))))
 (list (eqc (t-var 'wholeThing6) (t-bool)) (eqc (t-var 'zeroBody6798) (t-num)) (eqc (t-var 'zeroBody6798) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing7 (alpha-vary (parse '(bif false 43 true)))))
 (list (eqc (t-var 'wholeThing7) (t-var 'then15736)) (eqc (t-var 'test15735) (t-bool)) (eqc (t-var 'then15736) (t-var 'else15737)) (eqc (t-var 'test15735) (t-bool)) (eqc (t-var 'then15736) (t-num)) (eqc (t-var 'else15737) (t-bool))))

((constraint-list=? (generate-constraints 'wholeThing8 (alpha-vary (parse '(bif true 43 35)))))
 (list (eqc (t-var 'wholeThing8) (t-var 'then15739)) (eqc (t-var 'test15738) (t-bool)) (eqc (t-var 'then15739) (t-var 'else15740)) (eqc (t-var 'test15738) (t-bool)) (eqc (t-var 'then15739) (t-num)) (eqc (t-var 'else15740) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing9 (alpha-vary (parse '(rec (x 345) (+ x 1))))))
 (list (eqc (t-var 'wholeThing9) (t-var 'withBody6806))
       (eqc (t-var 'x6805) (t-var 'boundBody6807))
       (eqc (t-var 'boundBody6807) (t-num))
       (eqc (t-var 'withBody6806) (t-num))
       (eqc (t-var 'addlhs6808) (t-num))
       (eqc (t-var 'addrhs6809) (t-num))
       (eqc (t-var 'addlhs6808) (t-var 'x6805))
       (eqc (t-var 'addrhs6809) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing10 (alpha-vary (parse '(fun (x) (* x 2))))))
 (list (eqc (t-var 'wholeThing10) (t-fun (t-var 'x6810) (t-var 'bodyID6811)))
       (eqc (t-var 'bodyID6811) (t-num))
       (eqc (t-var 'addlhs6812) (t-num))
       (eqc (t-var 'addrhs6813) (t-num))
       (eqc (t-var 'addlhs6812) (t-var 'x6810))
       (eqc (t-var 'addrhs6813) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing11 (alpha-vary (parse '({fun (x) (* x 2)} 10)))))
 (list (eqc (t-var 'wholeThing11) (t-var 'funReturn6817))
       (eqc (t-var 'funExpr6815) (t-fun (t-var 'argExpr6816) (t-var 'funReturn6817)))
       (eqc (t-var 'argExpr6816) (t-num))
       (eqc (t-var 'funExpr6815) (t-fun (t-var 'x6814) (t-var 'bodyID6818)))
       (eqc (t-var 'bodyID6818) (t-num))
       (eqc (t-var 'addlhs6819) (t-num))
       (eqc (t-var 'addrhs6820) (t-num))
       (eqc (t-var 'addlhs6819) (t-var 'x6814))
       (eqc (t-var 'addrhs6820) (t-num))))
((constraint-list=? (generate-constraints 'wholeThing12 (alpha-vary (parse '(with (x (fun (y) (* y 2))) (x 10))))))
 (list (eqc (t-var 'wholeThing12) (t-var 'withBody6823))
       (eqc (t-var 'x6821) (t-var 'boundBody6824))
       (eqc (t-var 'boundBody6824) (t-fun (t-var 'y6822) (t-var 'bodyID6828)))
       (eqc (t-var 'bodyID6828) (t-num))
       (eqc (t-var 'addlhs6829) (t-num))
       (eqc (t-var 'addrhs6830) (t-num))
       (eqc (t-var 'addlhs6829) (t-var 'y6822))
       (eqc (t-var 'addrhs6830) (t-num))
       (eqc (t-var 'withBody6823) (t-var 'funReturn6827))
       (eqc (t-var 'funExpr6825) (t-fun (t-var 'argExpr6826) (t-var 'funReturn6827)))
       (eqc (t-var 'argExpr6826) (t-num))
       (eqc (t-var 'funExpr6825) (t-var 'x6821))))



;;Automated test cases
((constraint-list=? (generate-constraints 'test (parse 'x))) 
 (list (eqc (t-var 'test) (t-var 'x))))
((constraint-list=? (generate-constraints 'test (parse true))) 
 (list (eqc (t-var 'test) (t-bool))))
((constraint-list=? (generate-constraints 'test (parse '0))) 
 (list (eqc (t-var 'test) (t-num)))) 
((constraint-list=? (generate-constraints 'test (parse '(fun (a) (+ x 1))))) 
 (list (eqc (t-var 'test) (t-fun (t-var 'a) (t-var 'bodyID)))
       (eqc (t-var 'bodyID) (t-num))
       (eqc (t-var 'addlhs) (t-num))
       (eqc (t-var 'addrhs) (t-num))
       (eqc (t-var 'addlhs) (t-var 'x))
       (eqc (t-var 'addrhs) (t-num))))



;; --------------------------------------- unification ---------------------------------------------

;; Helper function: replace

;; Contract: replace : Type Type (listof Constraint) -> (listof Constraint)

;; Purpose: Takes the elements extracted from the top of the "stack" of constraints (first element from the list of the constraints),and replaces variable names on the rest of the stack (rest of the list of constraints) according to unification algorithm.

;; Examples: see tests

;; Definition [refines the header]:
(define (replace x y constraints)
  (local [(define (replace constraint)
            (cond
              [(eqc? constraint) (eqc (replace (eqc-lhs constraint)) (replace (eqc-rhs constraint)))]
              [(t-list? constraint) (cond
                                      [(t-list? (t-list-elem constraint)) (error 'unify "The list can't consist of lists: (t-list (t-list))")]
                                      [(t-fun? (t-list-elem constraint)) (error 'unify "The list can't consist of functions: (t-list (t-fun))")]
                                      [true (t-list (replace (t-list-elem constraint)))])]
              [(t-fun? constraint) (t-fun (replace (t-fun-arg constraint)) (replace (t-fun-result constraint)))]
              [(t-var? constraint) (if (equal? x constraint) y constraint)]
              [true constraint]))]
    (map replace constraints)))

;; Test:
'replace:
(test (replace (t-var 'element3078) (t-num) (list (eqc (t-var 'element3078) (t-num))))  (list (eqc (t-num) (t-num))))  ;;simple constraint replacement
(test (replace (t-var 'element3079) (t-num) (list (eqc (t-var 'element3078) (t-num))))  (list (eqc (t-var 'element3078) (t-num)))) ;;simple constraint replacement (nothing to replace)
(test (replace (t-var 'element3078) (t-num) (list (eqc (t-var 'element3078) (t-num))(eqc (t-var 'element3079) (t-bool))))
      (list (eqc (t-num) (t-num)) (eqc (t-var 'element3079) (t-bool))))                                                ;;list of 2 constraints - first replaced
(test (replace (t-var 'element3079) (t-num) (list (eqc (t-var 'element3078) (t-num))(eqc (t-var 'element3079) (t-bool))))
      (list (eqc (t-var 'element3078) (t-num)) (eqc (t-num) (t-bool))))                                                ;;list of 2 constraints - second replaced
(test (replace (t-var 'element3079) (t-num) (list (eqc (t-var 'element3078) (t-num))(eqc (t-var 'element3078) (t-bool))))
      (list (eqc (t-var 'element3078) (t-num)) (eqc (t-var 'element3078) (t-bool))))                                   ;;list of 2 constraints (nothing to replace)
(test (replace (t-var 'element3078) (t-num) (list (eqc (t-var 'element3078) (t-num))(eqc (t-var 'element3078) (t-bool))))
      (list (eqc (t-num) (t-num)) (eqc (t-num) (t-bool))))
(test (replace (t-var 't13819) (t-bool) (list (eqc (t-var 't13819) (t-bool)) (eqc (t-var 't13819) (t-list (t-var 't13819))) (eqc (t-var 't13820) (t-list (t-var 't13820))) (eqc (t-var 't13820) (t-num)) (eqc (t-var 't13819) (t-list (t-var 'ANYTHING))))) (list (eqc (t-bool) (t-bool)) (eqc (t-bool) (t-list (t-bool))) (eqc (t-var 't13820) (t-list (t-var 't13820))) (eqc (t-var 't13820) (t-num)) (eqc (t-bool) (t-list (t-var 'ANYTHING)))));; long list


;; Contract: unify : (listof Constraint) -> (listof Constraint)

;; Purpose: Implements the unification algorithm from class. The list of constraints that is returned should only have t-vars on the left.

;; Example: see test

;; Definition [refines the header]:
(define (unify loc)
  ;;build stack
  (local [(define (unify-helper loc subs)
            
            (define x (if (empty? loc) empty (eqc-lhs (first loc))))
            (define y (if (empty? loc) empty (eqc-rhs (first loc))))
            (if (empty? loc)
                (reverse subs)                       ;; since pushing on the "stack" reverses the order of constraints, we need to reverse it back
                
                (cond                            ;; algorithm steps begins
                  [(equal? x y)
                   (unify-helper (rest loc) subs)]                                                 ;; Step 1
                  
                  [(t-var? x)
                   (unify-helper (replace x y (rest loc)) (cons (eqc x y)(replace x y subs))) ]  ;; Step 2
                  [(t-var? y)
                   (unify-helper (replace y x (rest loc)) (cons (eqc y x)(replace y x subs))) ]  ;; Step 3
                  
                  [(and (t-list? x) (t-list? y))
                   (unify-helper (cons (eqc (t-list-elem x) (t-list-elem y)) (rest loc)) subs)]    ;; Step 4.1
                  
                  [(and (t-fun? x) (t-fun? y))
                   (unify-helper (cons (eqc (t-fun-arg x) (t-fun-arg y))
                                       (cons (eqc (t-fun-result x) (t-fun-result y))
                                             (rest loc))) subs)]    ;; Step 4.2
                  
                  [true (error 'unify "Unification error")]
                  
                  )
                ))]
    (unify-helper loc empty)))

;; Tests [most of the passing tests need to be verified manually because "alpha-vary" prevents from automating them]:
'unify:
(test (unify (list (eqc (t-num)(t-num))  (eqc (t-var 'element3078) (t-num)) (eqc (t-var 'element3078) (t-num))))
      (list (eqc (t-var 'element3078) (t-num))))
(test/exn (unify (list (eqc (t-var 'element3078) (t-num)) (eqc (t-var 'element3078) (t-num))(eqc (t-var 'element3078) (t-bool)))) "Unification error")
(test/exn (unify (list (eqc (t-var 'element3078) (t-num)) (eqc (t-var 'element3079) (t-num))(eqc (t-var 'element3078) (t-bool)))) "Unification error") 
(test (unify (generate-constraints 'x234 (num 1))) (list (eqc (t-var 'x234) (t-num))))
(test (unify (generate-constraints 'x543 (id 'x54))) (list (eqc (t-var 'x543) (t-var 'x54))) )
(test (unify (generate-constraints 'x123 (bool false))) (list (eqc (t-var 'x123) (t-bool))))
(test/exn (unify (generate-constraints 'wholeThing (bin-num-op + (bool false) (bool false)))) "Unification error")
(test/exn (unify (generate-constraints 'wholeThing (bin-num-op + (bool false) (num 2)))) "Unification error")
(unify (generate-constraints 'wholeThingProb (bin-num-op + (bin-num-op + (num 1) (num 2)) (num 3))))     
(test/exn (unify (generate-constraints 'zeroTest (iszero (bool false)))) "Unification error")
(unify (generate-constraints 'bifTest (bif (bool false) (num 2) (num 3))))
(unify (generate-constraints 'bifTest (bif (bool false) (bool false) (bool true))))
(test/exn (unify (generate-constraints 'bifTest (bif (bool false) (num 0) (bool true)))) "Unification error")
"unify : occurs check test"
(test (unify (list (eqc (t-var 'x) (t-list (t-var 'x)))))(list(eqc (t-var 'x) (t-list (t-var 'x)))))

'unify:lists
(unify (generate-constraints 'empptTest (tempty))) 
(test/exn (unify (generate-constraints 'consTest (tcons (num 1) (tcons (bool false) (tempty)))))  "Unification error")
(unify (generate-constraints 'firstTest (tfirst (tcons (num 1) (tempty)))))
(unify (generate-constraints 'restTest (trest (tcons (num 1) (tempty)))))
(test/exn (unify (generate-constraints 'restTest (trest (num 1)))) "Unification error")
(unify (generate-constraints 'isemptyTest (istempty (tcons (num 1) (tempty)))))

'unify:with
(unify (generate-constraints 'withTest (with 'x (num 1) (bin-num-op + (id 'x) (num 2)))))
(test/exn (unify (generate-constraints 'withTest (with 'x (bool true) (bin-num-op + (id 'x) (num 2))))) "Unification error")

'unify:functions
(unify (generate-constraints 'funTest (fun 'x (num 4))))
(unify (generate-constraints 'funTest2 (fun 'x (bin-num-op + (num 1) (id 'x)))))
(unify (generate-constraints 'funWithTest (with 'y (num 0)(fun 'x (bin-num-op + (num 1) (id 'x))))))
(test/exn (unify (generate-constraints 'funWithTest (with 'y (bool false)(fun 'x (bin-num-op + (id 'y) (id 'x))))))  "Unification error")
(unify (generate-constraints 'funWithTest (with 'y (num 0)(fun 'x (bin-num-op + (id 'y) (id 'x))))))


;; Contract: infer-type : Expr -> Type

;; Purpose: Extracts the type of substitution returned by the provided expression (passed as a first argument)

;; Examples: See Tests.

;; Definition [refines the header]:
(define (infer-type e)
  (eqc-rhs (first (unify (generate-constraints 'result (alpha-vary e)))))
  )

;; Tests:
'infer-type:custom
(define add1-fun '(fun (x) (+ x 1)))
(test/pred (infer-type (parse add1-fun)) (type=? (t-fun (t-num) (t-num)))) 
(test/pred (infer-type (parse `(,add1-fun 1))) (type=? (t-num))) 
(test/exn (infer-type (parse `(,add1-fun false))) "unify") 

'infer-type:primitives
((type=? (infer-type (parse '0))) (t-num))
((type=? (infer-type (parse true))) (t-bool))
((type=? (infer-type (parse #f))) (t-bool))

'infer-type:bin-num-op
((type=? (infer-type (parse '{+ 1 2}))) (t-num))
((type=? (infer-type (parse '{- {* 2 3} 4}))) (t-num))                    ;; nested primitive test
(test/exn ((type=? (infer-type (parse '{+ true 2})))) "unify")            ;; error test - not nested
(test/exn (type=? (infer-type (parse '{- {* 2 #f} 4}))) "unify")          ;; error test - nested primitive test
(test/exn (type=? (infer-type (parse '{- {* 2 3} #t}))) "unify")          ;; error test - nested primitive test
(test/exn (type=? (infer-type (parse '{- {* false 3} 6}))) "unify")       ;; error test - nested primitive test

'infer-type:iszero
((type=? (infer-type (parse '{iszero 0}))) (t-bool))                      ;;is zero simple cases
((type=? (infer-type (parse '{iszero 5}))) (t-bool))
(test/exn (type=? (infer-type (parse '{iszero false}))) "unify")          ;; is zero - simple error test
((type=? (infer-type (parse '{iszero [+ 1 [* 2  3]]}))) (t-bool))         ;; nested case
(test/exn (type=? (infer-type (parse '{iszero [+ 1 [* 2  false]]})))  "unify")          ;; nested case - error
(test/exn (type=? (infer-type (parse '{iszero [+ 1 [* 2  [iszero 0]]]})))  "unify")     ;; nested case - error
(test/exn (type=? (infer-type (parse '{iszero {iszero 0}})))  "unify")    ;; recursive case - error

'infer-type:bif
((type=? (infer-type (parse '{bif true false false}))) (t-bool))          ;;bif simple cases
((type=? (infer-type (parse '{bif true 1 2}))) (t-num))                   ;;bif simple cases
((type=? (infer-type (parse '{bif false x y}))) (t-var 'some-variable))   ;;bif simple cases
(test/exn (type=? (infer-type (parse '{bif 0 false false}))) "unify")     ;;bif - error in condition
(test/exn (type=? (infer-type (parse '{bif true false 1}))) "unify")      ;;bif - error:return type mismatch
((type=? (infer-type (parse '{bif x y x}))) (t-var 'some-variable))       ;;bif - labels

'infer-type:id
((type=? (infer-type (parse 'x))) (t-var 'stuff))

'infer-type:with
((type=? (infer-type (parse '{with [x 1] 0}))) (t-num))                    ;;with - simple test cases
((type=? (infer-type (parse '{with [x 1] #t}))) (t-bool))
((type=? (infer-type (parse '{with [x 1] t}))) (t-var 'stuff))
((type=? (infer-type (parse '{with [x 1] x}))) (t-num))
((type=? (infer-type (parse '{with [x 1] {+ x 2}}))) (t-num))              ;;with - combined
((type=? (infer-type (parse '{with [x 1] {with [y 2] {- x y}}}))) (t-num)) ;; nested with
((type=? (infer-type (parse '{with [x x] {with [y y] {- x y}}}))) (t-num)) ;; nested with     
((type=? (infer-type (parse '{with [x 1] {with [y x] {- x y}}}))) (t-num)) ;; nested with
(test/exn (type=? (infer-type (parse '{with [x false] {with [y 2] {- x y}}}))) "unify") ;; nested with - error
(test/exn (type=? (infer-type (parse '{with [x 1] {with [y #t] {- x y}}}))) "unify")    ;; nested with - error
(test/exn (type=? (infer-type (parse '{with [x 1] {with [y 2] {with [z true] {- x {* y z}}}}}))) "unify")    ;; nested with - error

'infer-type:rec
((type=? (infer-type (parse '{rec [x 1] 0}))) (t-num))                   ;;rec - simple test cases
((type=? (infer-type (parse '{rec [x 1] #t}))) (t-bool))
((type=? (infer-type (parse '{rec [x 1] t}))) (t-var 'stuff))
((type=? (infer-type (parse '{rec [x 1] x}))) (t-num))
((type=? (infer-type (parse '{rec [x 1] {+ x 2}}))) (t-num))             ;;rec - combined
((type=? (infer-type (parse '{rec [x 1] {rec [y 2] {- x y}}}))) (t-num)) ;; nested rec
((type=? (infer-type (parse '{rec [x x] {rec [y y] {- x y}}}))) (t-num)) ;; nested rec  
((type=? (infer-type (parse '{rec [x 1] {rec [y x] {- x y}}}))) (t-num)) ;; nested rec
(test/exn (type=? (infer-type (parse '{rec [x false] {rec [y 2] {- x y}}}))) "unify") ;; nested rec - error
(test/exn (type=? (infer-type (parse '{rec [x 1] {rec [y #t] {- x y}}}))) "unify")    ;; nested rec - error
(test/exn (type=? (infer-type (parse '{rec [x 1] {rec [y 2] {rec [z true] {- x {* y z}}}}}))) "unify")    ;; nested rec - error

'infer-type:fun
((type=? (infer-type (parse '{fun (x) 0}))) (t-fun (t-var 'stuff) (t-num)))           ;; simple functions
((type=? (infer-type (parse '{fun (x) x}))) (t-fun (t-var 'stuff) (t-var 'stuff)))
((type=? (infer-type (parse '{fun (x) true}))) (t-fun (t-var 'stuff) (t-bool)))
((type=? (infer-type (parse '{fun (x) y}))) (t-fun (t-var 'stuff) (t-var 'some-other-stuff)))
((type=? (infer-type (parse '{fun (x) {fun (y) {- x y}}}))) (t-fun (t-num) (t-fun (t-num) (t-num))))
(test/exn (type=? (infer-type (parse '{fun (x) {+ x{fun (y) true}}}))) "unify")       ;; function- errors
(test/exn (type=? (infer-type (parse '{fun {fun (y) true} 1}))) "parse")       ;; function- errors
(test/exn (type=? (infer-type (parse '{with (x true) {+ 1 {fun (y) x}}}))) "unify")   ;; function- errors
(test/exn (type=? (infer-type (parse '{with (x true) {+ 1 {fun (y) x}}}))) "unify")   ;; function- errors


'infer-types:app
((type=? (infer-type (parse '{x 0}))) (t-var 'stuff))           ;; simple app
((type=? (infer-type (parse '{x true}))) (t-var 'stuff))           ;; simple app
((type=? (infer-type (parse '{x x}))) (t-var 'stuff))           ;; simple app
(test/exn (type=? (infer-type (parse '{true x})))  "unify")            ;; simple app - error
(test/exn (type=? (infer-type (parse '{0 x})))  "unify")           ;; simple app - error
(test/exn (type=? (infer-type (parse '{0 1})))  "unify")           ;; simple app - error
(test/exn (type=? (infer-type (parse '{true false}))) "unify")           ;; simple app - error
((type=? (infer-type (parse '{{x 1} x}))) (t-var 'some))           ;; nested app
(test/exn (type=? (infer-type (parse '{{with [x 1] x} x}))) "unify") ;; combined app - error
((type=? (infer-type (parse '{{x 1} {with[x 1] x}}))) (t-var 'some))           ;; nested app
((type=? (infer-type (parse '{{fun (x) x} x}))) (t-var 'stuff))    ;; testing actual function applications
((type=? (infer-type (parse '{{fun (x) x} 1}))) (t-num))           ;; testing actual function applications
((type=? (infer-type (parse '{{fun (x) x} #t}))) (t-bool))         ;; testing actual function applications


'infer-type:tempty
((type=? (infer-type (parse 'tempty))) (t-list (t-var 'stuff)))           ;; simple tempty
((type=? (infer-type (parse '{trest {tcons 1 tempty}}))) (t-list (t-num)))  ;; tempty in a list
((type=? (infer-type (parse '{trest {tcons true tempty}}))) (t-list (t-bool)))  ;; tempty in a list
((type=? (infer-type (parse '{trest {tcons x tempty}}))) (t-list (t-var 'stuff)))  ;; tempty in a list

'infer-type:tcons
((type=? (infer-type (parse '{tcons x tempty}))) (t-list (t-var 'stuff)))           ;; list of t-var
((type=? (infer-type (parse '{trest {tcons 1 tempty}}))) (t-list (t-num)))  ;; list of t-num
((type=? (infer-type (parse '{trest {tcons true tempty}}))) (t-list (t-bool)))  ;;list of t-bool
(test/exn (type=? (infer-type (parse '{trest {tcons true false}}))) "unify")  ;;malformed list
(test/exn (type=? (infer-type (parse '{trest {tcons 1 2}}))) "unify")  ;;malformed list
(test/exn (type=? (infer-type (parse '{trest {tcons tempty 2}}))) "unify")  ;;malformed list
(test/exn (type=? (infer-type (parse '{trest {tcons tempty tempty}}))) "unify: The list can't consist of lists: (t-list (t-list))")  ;;malformed list

'infer-type:tempty?
((type=? (infer-type (parse '{tempty? tempty}))) (t-bool))           ;; simple tempty?
((type=? (infer-type (parse '{tempty? x}))) (t-bool))           ;; simple tempty?
(test/exn (type=? (infer-type (parse '{tempty? 1}))) "unify")           ;; simple tempty?
((type=? (infer-type (parse '{tempty? {tcons 1 tempty}}))) (t-bool))  ;; tempty? acted on tcons
((type=? (infer-type (parse '{tempty? {{fun (x) {tcons x tempty}} 1}}))) (t-bool))  ;; tempty? nested               
((type=? (infer-type (parse '{with [x {tcons x tempty}] {tempty? x}}))) (t-bool))  ;; tempty? nested               
(test/exn (type=? (infer-type (parse '{tempty? {fun (x) {x tempty}}}))) "unify")  ;; tempty? nested
((type=? (infer-type (parse '{with [x tempty] {tempty? x}}))) (t-bool))  ;; tempty? on the app through 'with'

'infier-type:trest
((type=? (infer-type (parse '{trest {tcons 1 tempty}}))) (t-list (t-num)))  ;; trest acted on a list
((type=? (infer-type (parse '{trest {tcons true tempty}}))) (t-list (t-bool)))  ;; trest acted on a list
((type=? (infer-type (parse '{trest {tcons x tempty}}))) (t-list (t-var 'stuff)))  ;; trest in a list
((type=? (infer-type (parse '{trest {{fun (x) {tcons x tempty}} #t}}))) (t-list (t-bool)))  ;; trest in a list  through 'fun'
(test/exn (type=? (infer-type (parse '{trest {fun (x) {x tempty}}}))) "unify")  ;; trest on app through 'fun'
((type=? (infer-type (parse '{with [x {tcons true tempty}] {trest x}}))) (t-list (t-bool)))  ;; trest nested through 'with'
((type=? (infer-type (parse '{with [x tempty] {trest x}}))) (t-list (t-var 'stuff)))  ;; trest nested through 'with'        
(test/exn (type=? (infer-type (parse '{trest {fun (x) {x tempty}}}))) "unify")  ;; trest on the app through 'with'

'infer-type:tfirst
((type=? (infer-type (parse '{tfirst {tcons x tempty}}))) (t-var 'stuff))           ;; list of t-var
((type=? (infer-type (parse '{tfirst {tcons 1 tempty}}))) (t-num))                  ;; list of t-num
((type=? (infer-type (parse '{tfirst {tcons true tempty}}))) (t-bool))                  ;; list of t-bool
((type=? (infer-type (parse '{tfirst {{fun (x) {tcons x tempty}} x}}))) (t-var 'stuff))  ;; tfirst in a list  through 'fun'
(test/exn (type=? (infer-type (parse '{tfirst {fun (x) {x tempty}}}))) "unify")  ;; tfirst on app through 'fun'
((type=? (infer-type (parse '{with [x {tcons 1 tempty}] {tfirst x}}))) (t-num))  ;; tfirst nested through 'with'
((type=? (infer-type (parse '{with [x tempty] {tfirst x}}))) (t-var 'stuff))     ;; tfirst nested through 'with'        
(test/exn (type=? (infer-type (parse '{tfirst {fun (x) {x tempty}}}))) "unify")  ;; tfirst on the app through 'with'


"EXTRA CREDIT"
(infer-type (parse '{fun (a) b}))